$\forall$$T$:Type, $m$:$\mathbb{N}$, $L$:$T$ List. $m$$<\parallel$$L$$\parallel$ $\Rightarrow$ nth\_tl($m$;$L$) $=$ ($L$[$m$].nth\_tl(1+$m$;$L$)) $\in$ $T$ List